((Unfold `p{-}co{-}restrict` 0) \\[0ex]CollapseTHEN (Auto$\cdot$))$\cdot$